import Mathlib

open Classical

structure FOL_QKB where
  Entity : Type
  World  : Type
  A      : World → World → Prop
  In     : Entity → World → Prop

local notation "𝓕" => FOL_QKB

namespace Axioms

def AxiomB     (frame : 𝓕) : Prop := ∀ w v, frame.A w v → frame.A v w
def AxiomAlpha (frame : 𝓕) : Prop := ∀ w v, (∀ a, ¬frame.In a w) ∧ (∃ b, frame.In b v) → ¬frame.A w v
def AxiomBeta  (frame : 𝓕) : Prop := ∃ a, ∀ b w v, ¬frame.In a v ∨ ¬frame.A w v ∨ ¬frame.In b w ∨ frame.In a w
def AxiomGamma (frame : 𝓕) : Prop := ∀ a, ∃ w, frame.In a w
def AxiomDelta (frame : 𝓕) : Prop := ∀ a, (∃ w v, frame.In a w ∧ ¬frame.In a v) → (∃ u t, frame.In a u ∧ ¬frame.In a t ∧ frame.A u t)

end Axioms

def ConclusionC (frame : 𝓕) : Prop := ∃ a, ∀ w, frame.In a w

theorem MainTheorem (frame : 𝓕)
    (ax_B     : Axioms.AxiomB     frame)
    (ax_alpha : Axioms.AxiomAlpha frame)
    (ax_beta  : Axioms.AxiomBeta  frame)
    (ax_gamma : Axioms.AxiomGamma frame)
    (ax_delta : Axioms.AxiomDelta frame)
    : ConclusionC frame := by
  -- Extract the entity 'a' whose F-relation is well-founded
  obtain ⟨a, ha⟩ := ax_beta
  refine ⟨a, ?_⟩
  -- Assume for reductio that 'a' is contingent
  by_contra h_not_necessary
  push Not at h_not_necessary
  obtain ⟨w_not_exist, h_not_In_a_w⟩ := h_not_necessary
  -- By Gamma, 'a' exists in some world
  obtain ⟨v_exist, h_In_a_v⟩ := ax_gamma a
  -- Hence 'a' is contingent in the sense required by Delta
  have h_contingent : ∃ w' v', frame.In a w' ∧ ¬frame.In a v' :=
    ⟨v_exist, w_not_exist, h_In_a_v, h_not_In_a_w⟩
  -- By Delta, some world 'u' where 'a' exists accesses 't' where it does not
  obtain ⟨u, t, h_In_a_u, h_not_In_a_t, h_A_u_t⟩ := ax_delta a h_contingent
  -- By B, 't' accesses 'u'
  have h_A_t_u : frame.A t u := ax_B u t h_A_u_t
  -- By Beta, 't' must be empty (eliminating the other three disjuncts)
  have h_t_empty : ∀ b, ¬frame.In b t := by
    intro b
    rcases ha b t u with h1 | h2 | h3 | h4
    · exact absurd h_In_a_u h1
    · exact absurd h_A_t_u h2
    · exact h3
    · exact absurd h4 h_not_In_a_t
  -- By Alpha, an empty world cannot access a non-empty world
  have h_u_nonempty : ∃ y, frame.In y u := ⟨a, h_In_a_u⟩
  have h_not_A_t_u : ¬frame.A t u :=
    ax_alpha t u ⟨h_t_empty, h_u_nonempty⟩
  -- Contradiction
  exact absurd h_A_t_u h_not_A_t_u